﻿// Jinx AJAX Framework
// Copyright (C) 2008 Blake Hegerle
//
// This program is free software: you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.
//
// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

namespace Formality.FormalSystem.Reasoning.RuleInference
{
    using FSub = FunctionSubstitution.Justification;
    using Core;

    public class Search : IJustificationSearch
    {
        public Search(Proposition Goal, Proposition Basis, Tuple<Proposition, bool>[] Premises)
            : this(Goal,Basis,(from p in Premises where p.Item2 select p.Item1).ToArray())
        { }

        public Search(Proposition Goal, Proposition Basis, Proposition[] Premises)
        {
            this.Goal = Goal;
            this.Basis = Basis;
            this.Premises = Premises;
        }

        #region IJustificationSearch Members

        Reasoning.Justification IJustificationSearch.Perform()
        {
            var Rules = Basis.AsRules.Take(2);

            var Attempts = (from R in Rules select Try(R, Goal));

            return Attempts.FirstOrDefault(j => j != null);
        }

        #endregion

        private readonly Proposition Goal, Basis;
        private readonly Proposition[] Premises;

        private Justification Try(Rule Rule, Proposition Goal)
        {
            return Try(Sub(Rule.Consequent, Goal), Rule, 0);
        }

        private FSub Sub(Proposition From, Proposition To)
        {
            return new FunctionSubstitution.Search(From, To, false).Perform();
        }

        private Justification Try(FSub Justification, Rule Rule, int Index)
        {
            if (Justification == null) return null;

            if (Index == Rule.Antecedents.Length)
                return new Justification();

            var Antecedent = Rule.Antecedents[Index];

            foreach (var Premise in Premises)
            {
                var Attempt = new FunctionSubstitution.Search(Antecedent, Premise, Justification.Search);

                var FinalJustification = Try(Attempt.Perform(), Rule, Index + 1);

                if (FinalJustification != null)
                    return FinalJustification;
            }

            return null;
        }
    }
}
